Casper CBC: State transition
0. Message justification
The binary relation$ m_1 \preceq m_2 \Leftrightarrow m_1 \in {\rm Justification}(m_2)defined over$ M.
Lemma: Irreflexivity of justifications
$ \nexists m \in M. m \in \rm{Justification}(m)
"Message can't justify itself"
Lemma: Justification is partially ordered
The binary relation$ m_1 \succeq m_2 \Leftrightarrow m_1 \in {\rm Justification}(m_2) is partially ordered.
Lemma: Justified message is in$ M^{n-1}
$ \forall n \in \N. \ \forall m, m'. \ m \in M^n \land {\rm justified}(m', m) \Rightarrow m' \in M^{n - 1}
Note that here we don't have$ n - 1 \in \N
Case analysis, whether$ n = 0or not.
Lemma: Justification is well-founded in M
$ \nexists f. \ \forall i. \ f(i) \in M \land {\rm justified}(f(i + 1), f(i))
Proof by contradiction.
$ \exists f
$ \forall i. \ f(i) \in M \land {\rm justified}(f(i + 1), f(i))
1. Immediately next message
Definition: Immediately next message
$ {\rm Immediately\_next\_message}: (\Sigma \times M) \rightarrow \{True, False\}
$ {\rm Immediately\_next\_message} (\sigma, m) = {\rm Justification}(m) \subseteq \sigma \land m \notin \sigma
Note: We can remove$ m \notin \sigma.
2. State difference
Lemma: State differences have immediately next messages
$ \forall \sigma, \sigma' \in \Sigma. \ \sigma \rightarrow \sigma' \land \sigma \neq \sigma'
$ \exists m \in \sigma' \backslash \sigma. \ {\rm Immediately\_next\_message} (\sigma, m)
proof by contradiction
the subgoal is
$ \exists m \in \sigma' \backslash \sigma. {\rm Justification}(m) \subseteq \sigma
now, assume the negation.
$ \forall m \in \sigma' \backslash \sigma. {\rm Justification}(m) \nsubseteq \sigma
hence,
$ \forall m \in \sigma' \backslash \sigma. \exists m' \in {\rm Justification}(m). m' \notin \sigma
$ \forall m \in \sigma' \backslash \sigma. \exists m' \in {\rm Justification}(m). m' \notin \sigma \land m' \in \sigma'
$ \forall m \in \sigma' \backslash \sigma. \exists m' \in {\rm Justification}(m). m' \in \sigma' \backslash \sigma
Because of Irreflexivity_of_justifications, $ m \neq m'.
This means that all message in the difference ($ \sigma' \backslash \sigma) justifies at least one of the others.
This implies that the binary relation$ m_1 \succeq m_2 \Leftrightarrow m_1 \in {\rm Justification}(m_2)defined over$ \sigma \in \Sigmais not transitive.
NB. This doesn't mean neither there is a minimal element nor$ \succeqis a total order on$ \sigma' \backslash \sigma.
3. State transition by immediately next message
We introduce an important lemma which explains a "single" state trantision in CBC-style distributed algorithm.
Lemma: State transition by immediately next message
$ \forall \sigma \in \Sigma, \forall m \in M, m \notin \sigma
$ {\rm Immediately\_next\_message} (\sigma, m) \Leftrightarrow \sigma \cup \{m\} \in \Sigma
Proof ($ \Rightarrow)
$ \exists n \in {\bf N}. \ \sigma \in \Sigma^n
Case1: $ {\rm Justification}(m) = \sigma
In this case, $ \sigma \cup \{m\} \in \Sigma^{n+1}
Case2: $ {\rm Justification}(m) \subset \sigma
e.g. $ \sigma = \{(1, a, \empty), (1, a, \{(1, a, \empty)\})\} \in \Sigma^2, m = (1, b, \{(1, a, \empty)\}) \in M^1
e.g. $ \sigma = \{(1, a, \empty), (1, a, \{(1, b, \empty)\})\} is not valid
e.g.$ \sigma = \{(1, a, \empty), (1, b, \empty)\} is valid
e.g. $ \sigma = \{(1, a, \empty), (1, a, \{(1, a, \empty)\})\} \in \Sigma^2, m = (1, b, \empty) \in M^0
e.g. $ \sigma = \{(1, a, \empty), (1, a, \{(1, a, \empty)\}), (1, a, \{(1, a, \empty), (1, a, \{(1, a, \empty)\})\}) \in \Sigma^3
$ m = (1, b, \{(1, a, \empty), (1, a, \{(1, a, \empty)\})\}) \in M^2
Now, $ \sigma' = {\rm Justification}(m) \in \Sigma^kand$ \sigma' \subset \sigma
Also,$ \forall m' \in \sigma'. \ {\rm Justification(m') \subset \sigma}
Then,$ \sigma' \cup \{m\} \in \Sigma^{k + 1}
Maybe
Then,$ \exists \sigma'' \subset \sigma. \ {\rm Justification(\sigma'')} = \sigma'
Proof ($ \Leftarrow)
$ \forall \sigma \in \Sigma, \forall m \in M, m \notin \sigma
$ \sigma \cup \{m\} \in \Sigma
$ \Rightarrow \exists n \in \N. \ \sigma \cup \{m\} \in \Sigma^n
$ \Rightarrow \forall m' \in \sigma \cup \{m\}. {\rm Justification}(m') \subseteq \sigma \cup \{m\}
$ \Rightarrow \forall m' \in \sigma \cup \{m\}. {\rm Justification}(m') \subseteq \sigma \cup \{m\}
$ \Rightarrow {\rm Justification}(m) \subseteq \sigma (by irreflexivity of jutification)
$ \Rightarrow {\rm Justification}(m) \subseteq \sigma \land m \notin \sigma
$ \Rightarrow {\rm Immediately\_next\_message} (\sigma, m)
4. Minimal transition
$ (\sigma, \sigma') \in {\rm minimal\_transitions} \Leftrightarrow |\sigma' \backslash \sigma| = 1
Proof ($ \Rightarrow) by contradiction.
$ \forall \sigma, \sigma' \in \Sigma. \ \sigma \rightarrow \sigma' \land \sigma \neq \sigma'
Subgoal:$ |\sigma' \backslash \sigma| > 1 \Rightarrow \exists \sigma'' \in \Sigma. \ \sigma \rightarrow \sigma \land \sigma'' \rightarrow \sigma \land \sigma \neq \sigma'' \land \sigma'' \neq \sigma'
By State differences have immediately next messages,
$ \exists m \in \sigma' \backslash \sigma. \ Immediately\_next\_message (\sigma, m)
By State transition by immediately next message, $ \sigma''s.t.$ \sigma'' = \sigma \cup \{m\}exists and this is the counterexample, leading to the contradiction.
Others
By State differences have immediately next messages and State transition by immediately next message,
$ \forall \sigma, \sigma'. \sigma \to \sigma' \Longrightarrow \exists \sigma_1, \sigma_2, ..., \sigma_n \in \Sigma \land \sigma \to \sigma_1 \to \sigma_2 \to ... \to \sigma'
By the momotonicity of the number of faults, this holds for future states where there are t equivocation or less.
The graph of possible state transitions for a certain$ nmessages
If each message does not justify each other, the number of patterns is$ n!
In general, there are restrictions on the order of some sets of messages
Any graph theory helps here?